import static org.junit.Assert.assertEquals;
import static org.junit.Assert.assertSame;
import static org.junit.Assert.assertTrue;

import java.io.File;
import java.io.IOException;

import model.BasicParameter;
import model.cnf.CNF;
import model.cnf.FileCNF;
import model.preprocessor.IllegalPreProcessorParameterException;
import model.preprocessor.PreProcessorParameter;
import model.preprocessor.PreProcessorResult;
import model.preprocessor.PreProcessorResultStatus;

import org.junit.Before;
import org.junit.Test;

import controller.preprocessor.PreProcessor;
import controller.preprocessor.ReViVal;

public class TestRevival {

	private File precDirectory;
	private ReViVal sat ;
	
	@Before
	public void setUp(){
		try {
			precDirectory = new File("preproc");
			
			sat = new ReViVal(precDirectory);
		} catch (IOException e) {
			e.printStackTrace();
			return;
		}
	}
	
	@Test
	public void testRevival(){
		assertTrue("revial use timeout", sat.hasTimeout());
	}
		
	@Test
	public void testGetCommandLine(){
		String cnfFile = "./tstcnf/unsat.cnf";
		String out = "./cnf/newcnf.cnf";
		PreProcessorParameter param = sat.getRevivalParameter();
		param.setTimeOut(BasicParameter.NO_DELAY);
		param.setOut(out);
		String tmp = PreProcessor.correctFormatForLinux(sat.getPath())+" " + PreProcessor.correctFormatForLinux(cnfFile)+" > "+PreProcessor.correctFormatForLinux(out);
		 
		
		String[] tab = sat.getCommandLine(cnfFile);
		assertEquals("wrong parameter : wrong path", tab[0], "/bin/sh");
		assertEquals("wrong parameter : wrong argument", tab[1], "-c");
		assertEquals("wrong parameter : wrong arg for bash", tab[2], tmp);
	
		param.setTimeOut(4000);
		tmp = PreProcessor.correctFormatForLinux(sat.getPath())+" "+ PreProcessor.correctFormatForLinux(cnfFile)+" "+ String.valueOf(param.getTimeOut() / 1000)+" > "+PreProcessor.correctFormatForLinux(out);
		
		tab = sat.getCommandLine(cnfFile);
		assertEquals("wrong parameter : wrong path", tab[0], "/bin/sh");
		assertEquals("wrong parameter : wrong argument", tab[1], "-c");
		assertEquals("wrong parameter : wrong arg for bash", tab[2], tmp);
	
	}
	
	@Test
	public void testDetectUnsat(){
		String cnfFile = "./tstcnf/unsat.cnf";
		String out = "./cnf/newcnf.cnf";
		PreProcessorParameter param = sat.getRevivalParameter();
		param.setOut(out);
		CNF cnf;
		try {
			cnf = new FileCNF(cnfFile);
		} catch (Exception e) {
			e.printStackTrace();
			return;
		}
	
		PreProcessorResult res;
		try {
			res = sat.evaluate(cnf);
		} catch (IllegalPreProcessorParameterException e) {
			e.printStackTrace();
			return;
		}
		assertSame("doesn't detect cnf is unsat", PreProcessorResultStatus.UNSATISFIABLE, res.getStatus());
	}
	
	@Test
	public void testSatInstance(){
		String cnfFile = "./tstcnf/sat.cnf";
		String out = "./cnf/newcnf.cnf";
		PreProcessorParameter param = sat.getRevivalParameter();
		param.setOut(out);
		CNF cnf;
		try {
			cnf = new FileCNF(cnfFile);
		} catch (Exception e) {
			e.printStackTrace();
			return;
		}
		
		PreProcessorResult res;
		try {
			res = sat.evaluate(cnf);
		} catch (IllegalPreProcessorParameterException e) {
			e.printStackTrace();
			return;
		}
		assertSame("problem with sat instance", PreProcessorResultStatus.OK, res.getStatus());
		
	}
	

	@Test
	public void testTimeOut(){
		String cnfFile = "./tstcnf/longue.cnf";
		String out = "./cnf/newcnf.cnf";
		PreProcessorParameter param = sat.getRevivalParameter();
		param.setTimeOut(BasicParameter.MIN_DELAY);
		param.setOut(out);
		CNF cnf;
		try {
			cnf = new FileCNF(cnfFile);
		} catch (Exception e) {
			e.printStackTrace();
			return;
		}
		
		PreProcessorResult res;
		try {
			res = sat.evaluate(cnf);
		} catch (IllegalPreProcessorParameterException e) {
			//e.printStackTrace();
			return;
		}
		assertSame("problem with the use of timeout", PreProcessorResultStatus.TIMEOUT_REACHED, res.getStatus());
	}
	
	@Test
	public void testCNFDoesntExist(){
		String cnfFile = "./tstcnf";
		String out = "./cnf/newcnf.cnf";
		PreProcessorParameter param = sat.getRevivalParameter();
		param.setOut(out);
		CNF cnf;
		try {
			cnf = new FileCNF(cnfFile);
		} catch (Exception e) {
			//e.printStackTrace();
			return;
		}
		
		PreProcessorResult res;
		try {
			res = sat.evaluate(cnf);
		} catch (IllegalPreProcessorParameterException e) {
			//e.printStackTrace();
			return;
		}
		assertSame("doesn't detect problem", PreProcessorResultStatus.PROBLEM, res.getStatus());
	}
	
}
